FDL - Step of Proof: can-apply-fun-exp-add-iff

Step of Proof: can-apply-fun-exp-add-iff

Inference at * 2 1
Iof proof for Lemma can-apply-fun-exp-add-iff:

1. A : Type
2. n :

3. m :

4. f : A

(A + Top)
5. x : A
6. (

can-apply(f^m;x)) & (

can-apply(f^n;do-apply(f^m;x)))

can-apply(f^n o f^m ;x)

by ((Unfold `can-apply` ( 0)

)

CollapseTHEN (((RepUR ``p-compose`` ( 0)

)

CollapseTHEN (((((

C(if (0) =0 then SplitOnConclITE else SplitOnHypITE (0))

)
CollapseTHENA (Auto

))

)

ColCollapseTHEN ((((Try (Fold `can-apply` 0))

)
CCollapseTHEN (Auto

))

))

))

))

CC.

Definitions f o g , Unit, , tt, p q, p q, p q, [d], a < b, x f y, f(a), a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, P Q, suptype(S; T), left + right, S T, Top, x:A.B(x), Void, b, , , ff, x:A. B(x), t T, s = t, do-apply(f;x), can-apply(f;x), f^n, P & Q, x:A B(x), b, x:AB(x), , Type, A, P Q, False

Lemmas eqtt to assert, iff transitivity, eqff to assert, assert of bnot, can-apply wf, p-fun-exp wf, top wf, member wf, bool wf, bnot wf, not wf, assert wf